a, b:. ((0 < a & 0 < b)  (0 < -(a) & 0 < -(b)))  0 < a * b 

latex

Definitions	i <z j, ff, tt, if b then t else f fi , {T}, b, T, True, x. t(x), t  T, P  Q, , P  Q, P & Q, P  Q, P  Q, x:A. B(x), False, A, qpositive(r), x(s), S  T
Lemmas	qmul comm qrng, qmul zero qrng, bool wf, qminus positive, q trichotomy, qinv inv q, true wf, squash wf, qmul over minus qrng, qmul positive, assert-qpositive, and functionality wrt iff, or functionality wrt iff, iff functionality wrt iff, qpositive wf, assert wf, qmul wf, int inc rationals, qless wf, iff wf, rationals wf, all functionality wrt iff